∀E sknpk RW;
∀E reflex RW,S,0;
⊃E ↑↑,↑;
∃E ↑ w1;
∀E agree RW,w1;
∀E initial2 RW,w1;
∀E reflex RW,SP,0;
∀E ok2 w1;
TAUT ok(M(w1),N(w1))∧((M(w1)*N(w1))=(M(RW)*N(RW))∧¬(M(RW)=M(w1)∧N(RW)=N(w1))) 4:8;
SUBST rw1 IN ↑;
SUBST rw2 IN ↑;
∃I ↑ N(w1)←n M(w1)←m;
ASSUME ok(m,n)∧(m+n)=(m0+n0);
SUBSTR rw1 IN ↑;
SUBSTR rw2 IN ↑;
∀E sknpk w;
∀E initial3 RW,m,n;
∀E reflex RW,SP,0;
TAUTEQ ∃w1.(A(RW,w1,S,0)∧(M(w1)=m∧N(w1)=n)) 15:18;
∃E ↑ w;
TAUT ∃w1.(A(w,w1,P,0)∧¬agree(w,w1)) 16,20;
∃E ↑ w1;
∀E agree w,w1;
∀E initial2 w,w1;
∧E 20:#1;
∀E sp1 RW,w,0;
TAUT (M(w1)*N(w1))=(M(w)*N(w)) 22:26;
∀E ok2 w1;
∧E 20:#2;
∧E ↑:#1;
∧E ↑↑:#2;
TAUT ¬(M(w)=M(w1)∧N(w)=N(w1)) 22:23;
∧I (28 27 32);
SUBSTR 30 IN ↑;
SUBSTR 31 IN ↑;
∃I ↑ N(w1)←n1 M(w1)←m1;
⊃I 13⊃↑;
∀I ↑ m n;
∃E nsk w;
∀E agree RW,w;
TAUT ¬(M(RW)=M(w)∧N(RW)=N(w)) 39:40;
∀E initial1 RW,w;
∀E reflex RW,SP,0;
∀E ok2 w;
TAUT ok(M(w),N(w))∧((M(w)+N(w))=(M(RW)+N(RW))∧¬(M(RW)=M(w)∧N(RW)=N(w))) 39:44;
SUBST rw1 IN ↑;
SUBST rw2 IN ↑;
∃I ↑ N(w)←n M(w)←m;